\documentclass[xcolor=dvipsnames,mathserif,svgnames,11pt]{beamer}

% for a handout:
%
%\documentclass[handout,11pt]{beamer}
%
%\usepackage{pgfpages}
%\pgfpagesuselayout{2 on 1}[letterpaper,border shrink=5mm]


\usepackage{diagrams}
\usepackage{listings}
\usepackage{proof}
\lstdefinelanguage{MyHaskell}
{alsoletter={+,|,->, =, ::}, morekeywords={+,|,->, =, ::, data, Int, max, case, of}
}


\lstdefinelanguage{MyLambda}
{alsoletter={\., |, ->, = }, morekeywords={=,|, -> ,\., lam , fix, case, of}}


%\lstset{language=MyHaskell, keywordstyle=\color{scyan},basicstyle=\ttfamily}

\definecolor{syellow}{RGB}{181,137,0}
\definecolor{scyan}{RGB}{42,161,152}

\DefineNamedColor{named}{MyBlue}{RGB}{38,139,210}
\DefineNamedColor{named}{Base3}{RGB}{253,246,227}
\DefineNamedColor{named}{Base00}{RGB}{101,123,131}
\newcommand{\cemph}[1]{\textcolor{Blue}{#1}}
\newcommand{\remph}[1]{\textcolor{Blue}{#1}}
\newcommand{\uemph}[1]{\underline{#1}}
\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 

\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\include{seppp_annotated}
\mode<presentation>
{
  %\usetheme{Warsaw}
  % or ...
%gets rid of bottom navigation bars
%\setbeamertemplate{footline}[page number]{}

%gets rid of navigation symbols
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\usetheme{default}
%\usecolortheme[named=MyBlue]{structure}
%\setbeamercolor{background canvas}{bg=Base3}
%\setbeamercolor{normal text}{fg=Base00}

%\usetheme{Edinburgh}

%  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\title[Comp]
{Lambda Encoding, Types and Confluence}

\author{Peng Fu }

\institute[University of Iowa]
{ Advisor: Prof. Aaron Stump \\ 
  Dept. of Computer Science\\ }
\date{}
%\date{May 22, 2013 }
% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
%  \begin{frame}<beamer>
%    \frametitle{Outline}
%    \tableofcontents[currentsection,currentsubsection]
%  \end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

%% \begin{frame}
%% \frametitle{Prelude: Programs and Data}

%%     \begin{figure}
%%      \includegraphics{von-neumann.jpeg}
%%      \end{figure}
%% \end{frame}

%% \begin{frame}[fragile]
%% \frametitle{Prelude: Programs and Data}
%%     Buffer overflow(Data as Program)
%%     \begin{lstlisting}[language=C,keywordstyle=\color{SeaGreen},basicstyle=\ttfamily]
%%       #include <string.h>
%%       void foo (char *bar)
%%       {
%%         char  c[12];
%%         strcpy(c, bar);  // no bounds checking...
%%       }
%%       int main (int argc, char **argv)
%%       {
%%         foo(argv[1]); 
%%       }
%%     \end{lstlisting}
%% \end{frame}

\begin{frame}
\frametitle{Prelude: Programs and Data}
\begin{itemize}
\item<1-> Program as data
\item<2-> Data as Program?
\item<3-> $ 2\ f\ a \ = f\ (f\ a)$.
\item<4-> Lambda Calculus 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item \remph{Typed Lambda Calculus and Lambda Encoding}
%\item Typed Lambda encoding
\item Type Preservation and Confluence
\item Limits of Dependent type
\item Selfstar
\item Summary
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Lambda Calculus}

How to describe the \textit{plus one} function.
\begin{itemize}
\item $x+1$ 
\item $\xi+1$ (Frege, Grundgesetze der Arithmetik) 
\item $\hat{x}+1$ (Principia Mathematica)
\item $\hat{x}.x+1$ (Church)\footnote{Come from Barendregt's Impact of Lambda Calculus}
\item $\wedge x.x+1$ ( Typewriter)
\item $\lambda x.x+1$ (Modern) 
\item $x+1$ v.s. $\lambda x. x+1$

\end{itemize}


\end{frame}

%% \begin{frame}
%% \frametitle{Introduction: Lambda Calculus}

%% How about calling a function with an argument
%% \begin{itemize}
%% \item<1-> $f(a) = a + 1$ math
%% \item<2-> $(\lambda x.x+1)\ a \to_{\beta} a+1$ with lambda calculus
%% \item<3-> Explicit functional abstraction and application at syntactic level
%% \end{itemize}
%% \end{frame}


%% \begin{frame}
%% \frametitle{Introduction: Lambda Calculus}

%% Different angle to study lambda calculus


%% \begin{itemize}
%% \item<1-> Lambda calculus as foundation for mathematics. 
      
%% \item<2-> Semantics of lambda calculus

%% \item<3-> As a programming language with variant of $\beta$-reduction as 
%% operational semantics.

%% \item<4-> we will focus on the last angle.


%% \end{itemize}
%% \end{frame}

\begin{frame}
\frametitle{Lambda Calculus}

Higher order expression reduction system
\begin{itemize}
\item Terms(expression) $t \ ::= \ x \ | \ \lambda x.t \ | \ t \ t'$
      
\item Reduction  $(\lambda x.t)t' \to_{\beta} [t'/x]t$

\item In what sense it is higher order? 

\item Bind and free variable are primitives. 

free variable of $\lambda x.x\ y$ is $y$, $x$ is called bind variable. 

\item Variable binding in $\lambda x.\lambda y. x\ y \equiv \lambda z.\lambda x.z\ x$

$\lambda x.x \equiv \lambda y.y$

\item Reduction examples:

$(\lambda x.x)\ y \to_{\beta} y$

 $(\lambda x.x\ x)\ y \to_{\beta} y\ y$.


\end{itemize}
\end{frame}

\begin{frame}
\frametitle{  Lambda Calculus}



\begin{itemize}
\item To express higher order function 
      
\item Semantically, for an $a \in A$, $g: (A \to A) \to A$, where $f \mapsto f(a)$. 

\item With Lambda Calculus:

 $g \ := \lambda y. y\ a$

 $g\ f \equiv (\lambda y.y\ a)\ f \to_{\beta} f\ a$

\item Function $g$ is emulated at the syntactic level.

\end{itemize}


\end{frame}
\begin{frame}
\frametitle{  Types}


\begin{itemize}
\item Originated from Russell works, later used by Curry, Church and many others.
\item Now common in programming language. 
\item E.g. types in C, java. Central in Ocaml, Haskell.
\item Used to express certain assumptions, e.g. $\mathsf{String} \to \mathsf{int}$
\item The notion of types can be generalized to some sophisticated types, leads to theorem provers like Coq, Agda.
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Typed Lambda Calculus}

\only<1>{
Type is expression to govern the form
of lambda term: $\Gamma \vdash t:T$ 
\begin{itemize}
\item<1-> Simple type: $T\ ::= X \ | \ T \to T'$

\item<1-> Context(Environment) $\Gamma \ ::= \ \cdot \ | \ \Gamma, x : T $

\item<1-> Typing
\begin{figure}
\begin{tabular}{ll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&

\infer[\textit{Abs}]{\Gamma \vdash \lambda x.t :T_1 \to
T_2}{\Gamma, x:T_1 \vdash t: T_2}

\\
\\
\infer[\textit{App}]{\Gamma \vdash t\ t': T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

\\
\end{tabular}
\end{figure}
\end{itemize}
%% \item<2-> Polymorphic type 
%% \item<3-> Dependent type
%% \item<4-> Recursive type


%% \end{itemize}
}
\only<2>{
Extend simple type:
\begin{itemize}
\item<2-> Polymorphic type: $T\ ::= ... \ | \ \forall X:\kappa.T$
\item<2-> Kind: $\kappa \ ::= \ *$ 
\item<2-> Context: $\Gamma \ ::= ... \ | \ X:\kappa$
\item<2-> Typing
\begin{figure}
\begin{tabular}{ll}
    
\infer[\textit{Gen}]{\Gamma \vdash t:\forall X:\kappa.T}{\Gamma, X:\kappa \vdash t:T}

&

\infer[\textit{Inst}]{\Gamma \vdash t :[T'/X]T
}{\Gamma \vdash t: \forall X:\kappa. T & \Gamma \vdash T':\kappa}

\\
\end{tabular}
\end{figure}
\end{itemize}


}

\only<3>{
Extends Polymorphic type(System F): 
\begin{itemize}
\item<3-> Product type(dependent type): $T\ ::= ... \ | \ \Pi x:T.T' \ | \ T\ t$
\item<3-> Kind: $\kappa \ ::= \ * \ | \ \xi x:T.\kappa$. 
\item<3-> Typing
\begin{figure}
\begin{tabular}{l}
    
\infer[\textit{Pi}]{\Gamma \vdash \lambda x.t:\Pi x: T'.T}{\Gamma,x:T' \vdash t:T & x \in FV(T)}

\\
\\
\infer[\textit{Elim}]{\Gamma \vdash t\ t' :[t'/x]T}{\Gamma \vdash t: \Pi x:T'.T & \Gamma \vdash t':T' }
\\
\\

\infer[\textit{Conv}]{\Gamma \vdash t:[t_2/x]T}{\Gamma \vdash t:[t_1/x]T & t_1 =_{\beta} t_2}




\\
\end{tabular}
\end{figure}
\end{itemize}


}

\only<4>{
  Why Dependent Types?
  \begin{itemize}
  \item<4-> Curry-Howard correspondent for $\Gamma \vdash t:T$ 
$<\mathsf{Environment}>\ \vdash \  <\mathsf{program}>: <\mathsf{type}>$

$<\mathsf{Assumptions}>\ \vdash \  <\mathsf{proof}>: <\mathsf{formula}>$

  \item<4-> Type Preservation:

 If $\Gamma \vdash t:T$ and $t \to_{\beta} t'$, then $\Gamma \vdash t':T$.

  \item<4-> Strong Normalization:

 If $\Gamma \vdash t:T$, then there is no infinite beta reduction sequence.
  \end{itemize}


}
\end{frame}


\begin{frame}[fragile]
\frametitle{Algebraic Data types}

An example in Haskell: 

\begin{lstlisting}[language=MyHaskell, keywordstyle=\color{Blue},basicstyle=\ttfamily]
data Nat = Zero
          | Succ Nat

add :: Nat-> Nat -> Nat
add n m = case n of
          Zero -> m
         | Succ p -> add p (Succ m)

data List a = Nil | Cons a (List a)
data Tree = Empty
          | Leaf Int
          | Node Tree Tree
\end{lstlisting}

\end{frame}

\begin{frame}
\frametitle{  Core Language Design}
To support (algebraic) data type, one way is 
to add data type and pattern matching(to core) as primitive.
\begin{itemize}
\item<1-> expression for data type declaration:

$\mathsf{data}\ T\ (a_i:A_i)_{i\in I}: A\ \mathsf{where}\ \{ C_i:A_i\}_{i\in I}$
\item<1-> expression for pattern matching :

$\mathsf{case} \ a\ \mathsf{of} \ \{ C_i (x_1,...x_u)\ \Rightarrow\ a \}_{i\in I}$

\item<2-> Now typing rule become: 

{\tiny $\SepppdruleTBXXBranch{}$}

\end{itemize}
\end{frame}

\begin{frame}
\frametitle{  Core Language Design}


Complicate the analysis for core language.
\begin{itemize}
\item Type Preservation Proof for Standard ML
\item \textit{The machine-assisted proof of programming language properties}, 1996, Ph.D thesis by M. 
VanInwegen. 
\item Machine assisted proof by HOL.
\item Quoted from abstract: 

``We were not able to complete the proof of
type preservation because it is not true: we found counterexamples.''



\item In Haskell Core Language \footnote{http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/CoreSynType}: 

``Case expressions are the most complicated bit of Core. '' 

\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{  Scott Numerals}

\begin{itemize}

\item<1-> Scott encoding with Recursive Definition: 
\begin{lstlisting}[language=MyLambda, keywordstyle=\color{Blue},basicstyle=\ttfamily]
 Zero = lam s . lam z . z
 Succ n =  lam s . lam z . s n
 add n m = case n of 
              Zero -> m
            | Succ p -> add p (Succ m)
 pred n  = case n of 
              Zero -> Zero
            | Succ p -> p

\end{lstlisting}
\item<2-> Translate to lambda calculus with recursive definition

$\mathsf{Zero}\ := \lambda s.\lambda z.z$

$\mathsf{Succ}\ := \lambda n. \lambda s.\lambda z.s\ n$

$\mathsf{add}\ := \lambda n.\lambda m. n\ (\lambda p. \mathsf{add}\ p\ (\mathsf{Succ}\ m))\ m$

$\mathsf{pred}\ := \lambda n. n\ (\lambda p. p)\ \mathsf{Zero}$
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{  Scott Numerals}

\begin{itemize}
\item Isn't it great? No primitive data type and pattern matching needed!
\item Beta reduction and definition unfolding are enough.
\item the catch(or is it?): need recursive type and operation on Scott encoding data can not be typed in polymorphic type system. 
\begin{figure}
\begin{tabular}{ll}
    
\infer[\textit{Fold}]{\Gamma \vdash t:\mu X.T}{\Gamma \vdash t:[\mu X.T/X]T}

&

\infer[\textit{unFold}]{\Gamma \vdash t :[\mu X.T/X]T
}{\Gamma \vdash t: \mu X. T}
\\
\end{tabular}
\end{figure}
\item

\noindent $\mathsf{Nat} \ := \mu X. (X \to U) \to U \to U$ for any type $U$.

\noindent $\cdot \vdash \mathsf{add}:\mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Nat}$. 

\noindent $\cdot \vdash \mathsf{Zero}: \mathsf{Nat}$.

\noindent $\cdot \vdash \mathsf{Succ}: \mathsf{Nat} \to \mathsf{Nat}$.  
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{  Church Numerals}
Idea, $((2\ f)\ a)\ = f\ (f\ a)$, so $2 := \lambda f.\lambda a. f\ (f\ a)$.
\begin{itemize}
\item Church encoding 
\begin{lstlisting}[language=MyLambda, keywordstyle=\color{Blue},basicstyle=\ttfamily]
 Zero = lam s . lam z . z
 Succ n =  lam s . lam z . s (n s z)
 iterator n f a = n f a
 add n m = iterator n Succ m
\end{lstlisting}

\item One can see 

$1\ = \mathsf{Succ}\ \mathsf{Zero} \to_{\beta}^* \lambda s. \lambda z. s\ z$

$2\ = \mathsf{Succ}\ 1 \to_{\beta}^* \lambda s. \lambda z.s\ (s\ z)$

\item Easily translated to lambda calculus.
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{  Church Numerals}

\begin{itemize}
\item This is also great. 
\item Even better, it can be typed in system F(Polymorphic type). 

\noindent $\mathsf{Nat} \ := \forall X:*. (X \to X) \to X \to X$

\noindent $\cdot \vdash \mathsf{Succ} : \mathsf{Nat} \to \mathsf{Nat}$ 

\noindent $\cdot \vdash \mathsf{iterator} : \forall X:*. \mathsf{Nat} \to (X \to X) \to X \to X$ 

\noindent $\cdot \vdash \mathsf{add} :  \mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Nat}$ 

\item The catch, inefficient predecessor.
\item The predecessor function takes linear time(beta reductions) to compute, 
while with Scott encoding it only takes constant time. 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Typed Lambda Calculus and Lambda Encoding
%\item Typed Lambda encoding
\item \remph{Type Preservation and Confluence}
\item Limits of Dependent type
\item Selfstar
\item Summary
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{ Abstract Reduction System}

\begin{itemize}
\item Abstract Reduction System(ARS):
$(\mathcal{A}, \{ \to_{i}\}_{i \in \mathcal{I}})$
\item Basic concepts: 
 $a \stackrel{*}{\to}_i b$(or $a {\twoheadrightarrow}_i b$), $a =_i b$, \textit{reducible}, \textit{normal form}. 
\item Confluence and Church-Rosser property: 

$\to \ := \bigcup_{i\in \mathcal{I}} \to_i$. 

\

\begin{tabular}{lll}
\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldOnto & & \rdOnto &  \\
 b & &  &  & c \\
 & \rdDashtoo & & \ldDashtoo &  \\
 & & d & & \\
\end{diagram}

&
iff
&
\begin{diagram}[size=1.5em,textflow]
 a & & = &  & b \\
 & \rdDashtoo & & \ldDashtoo &  \\
 & & c & & \\
\end{diagram}

\end{tabular}


\end{itemize}  
\end{frame}


\begin{frame}
\frametitle{Confluence and Type Preservation }

\begin{itemize}
\item<1-> Recall type preservation: 

If $\Gamma \vdash t:T$ and $t \to t'$, then $\Gamma \vdash t':T$. 

Usually prove by induction on derivation of $\Gamma \vdash t:T$. 

\item<2-> Need to analyze the case: 

  \begin{tabular}{l}
    \infer[\textit{App}]{\Gamma \vdash (\lambda x.t)t':T}{\Gamma \vdash \lambda x.t:T'\to T & \Gamma \vdash t':T'}
  \end{tabular}

\item<3-> Present of non-syntax directed rule:

  \begin{tabular}{l}
    \infer[\textit{Conv}]{\Gamma \vdash t:T}{\Gamma \vdash t:T' & T = T'}
  \end{tabular}
\item<3-> Inversion on $\Gamma \vdash \lambda x.t:T'\to T$ gives us only:
$\Gamma, x:T_1 \vdash t: T_2$ where $T_1 \to T_2 = T'\to T$.
\item<4-> Want \textit{inverse structure congruence}:  

If $T_1 \to T_2 = T_1' \to T_2'$, then $T_1 = T_1'$ and $T_2 = T_2'$. 

\item<5-> By induction on derivation of $T_1 \to T_2 = T_1' \to T_2'$, case:

  \begin{tabular}{l}
    \infer[\textit{Trans}]{T_1 \to T_2 = T_1' \to T_2'}{T_1 \to T_2 = T_3 & T_3 = T_1' \to T_2'}
  \end{tabular}

\item<6-> Can't apply induction hypothesis! 

\end{itemize}  
\end{frame}


\begin{frame}
\frametitle{Confluence and Type Preservation }
Inverse structure congruence: 

If $T_1 \to T_2 = T_1' \to T_2'$, then $T_1 = T_1'$ and $T_2 = T_2'$. 

\begin{itemize}
\item We can define $=$ to be the reflexive, symmetric, transitive closure of $\rightarrowtail$.
\item We show that $\rightarrowtail$ is confluent, thus Church-Rosser. 
\item So $T_1 \to T_2 = T_1' \to T_2'$ implies there is a $T_3$ such that $T_1 \to T_2 \stackrel{*}{\rightarrowtail}  T_3$ and $T_1' \to T_2' \stackrel{*}{\rightarrowtail}  T_3$. 
\item We design $\rightarrowtail$ in such a way that $T_a \to T_b \rightarrowtail T$ iff 
$T \equiv T_a' \to T_b$ or $T \equiv T_a \to T_b'$, where $T_a \rightarrowtail T_a'$, $T_b \rightarrowtail T_b'$. 
\item Thus we conclude inverse structure congruence, conquered one problem for proving 
type preservation. 
%\item<6-> We apply this method to show type preservation of $\mathsf{Selfstar}$.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Confluence: Tait-Martin L\"of's Method}

Lambda calculus $(\Lambda , \to_{\beta})$ as ARS is confluent.

\begin{itemize}
\item<1-> Diamond property:
\begin{tabular}{lll}
\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo & & \rdTo &  \\
 b & &  &  & c \\
 & \rdDashto & & \ldDashto &  \\
 & & d & & \\
\end{diagram}
& implies &
\begin{diagram}[size=1.5em,textflow]
   &            &     &          & a  &            &  &            & & \\
   &            &     & \ldTo &   & \rdTo &   &  & & \\
   &            & c_1 &          &   &          & c_2 &            & & \\
   &  \ldTo     &     & \rdDashto        &   &       \ldDashto    &  &   \rdTo      & & \\
  e &            &     &            & d &           &   &           & b &  \\
   & \rdDashto &   & \ldDashto &   & \rdDashto &   & \ldDashto & & \\
   &            & c_1 &          &   &            & c_2 &            & & \\
   &            &  & \rdDashto         &   &    \ldDashto        &  &            & & \\
   &            &     &          & c  &            &  &            & & \\
\end{diagram}
\end{tabular}
\end{itemize}  
\end{frame}

\begin{frame}
\frametitle{Confluence: Tait-Martin L\"of's method}


$\to_{\beta}$ reduction does not have diamond property.

\begin{diagram}[size=1em,textflow]
 & & (\lambda x.f\ x\ x)\ ((\lambda y.y\ z)\ u) & & \\
 & \ldTo & & \rdTo &  \\
 f\ ((\lambda y.yz) u)((\lambda y.yz) u) & &  &  & (\lambda x.f\ x\ x)(u\ z) \\
 & \rdDashto & & \ldDashto &  \\
 & & ? & & \\
\end{diagram}

Not joinable in one step, but joinable in ``many'' steps. 

\end{frame}

\begin{frame}
\frametitle{Confluence: Tait-Martin L\"of's method}

\begin{itemize}
\item Parallel Reduction(a notion of ``many'' steps). 
  \begin{tabular}{l}
\infer{(\lambda x.t_1) t_2 \Rightarrow_{\beta} [t_2'/x]t_1' }{t_1 \Rightarrow_{\beta} t_1' & t_2 \Rightarrow_{\beta} t_2'}
\\    
  \end{tabular}

\item It has diamond property.

\item $\to_{\beta} \subseteq \Rightarrow_{\beta} \subseteq \stackrel{*}{\to_{\beta}}$, which implies $(\stackrel{*}{\to_{\beta}})\ =\ (\stackrel{*}{\Rightarrow_{\beta}})$ 

\item Confluence of $\Rightarrow_{\beta}$ implies confluence of $\to_{\beta}$
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Confluence: Takahashi's method}

\begin{itemize}
\item A stronger property, triangle property:

  \begin{tabular}{lll}

\begin{diagram}[size=1.5em,textflow]
 & & t & & \\
 &  & & \rdImplies &  \\
  & & \dMapsto &  & t' \\
 &  & & \ldEImplies &  \\
 & & t^* & & \\
\end{diagram}
 
& implies &
\begin{diagram}[size=1.6em,textflow]
 & & t & & \\
 & \ldImplies & & \rdImplies &  \\
 t_1 & & \dMapsto &  & t_2 \\
 &\rdEImplies  & & \ldEImplies &  \\
 & & t^* & & \\
\end{diagram}
    
  \end{tabular}

\item Parallel contractions:

\noindent  $x^* \ := \ x$.

\noindent  $(\lambda x.t)^* \ := \ \lambda x. t^*$.

\noindent  $(t_1\ t_2)^* \ := \ t_1^* \ t_2^*$ if $t_1 \ t_2$ is not a beta redex.

\noindent  $((\lambda x.t_1)\ t_2)^* \ := \ [t_2^*/x]t_1^* $.


\end{itemize}  
\end{frame}


\begin{frame}
\frametitle{Confluence: Barendregt's method}

\begin{itemize}
\item Strip property:
\begin{tabular}{lll}
\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo & & \rdOnto &  \\
b & &  &  & c \\
 & \rdDashtoo & & \ldDashtoo &  \\
 & & d & & \\
\end{diagram}

& implies &
\begin{diagram}[size=1.5em,textflow]
   &            &     &          & a  &            &  &            & & \\
   &            &     & \ldTo &   & \rdOnto &   &  & & \\
   &            & c_1 &          &   &          & b &            & & \\
   &  \ldTo     &     & \rdDashtoo        &   &       \ldDashtoo    &  &         & & \\
  e &            &     &            & d &           &   &           &  &  \\
   & \rdDashtoo &   & \ldDashtoo &   &  &   &  & & \\
   &            & c_1 &          &   &            &  &            & & \\
   &            &  &     &   &            &  &            & & \\
   &            &     &          &   &            &  &            & & \\
\end{diagram}

\end{tabular}

\end{itemize}  
\end{frame}


%% \begin{frame}
%% \frametitle{Confluence: Barendregt's labelling method}


%% \begin{itemize}

%% \item Extend lambda term to include $(\underline{\lambda}x.t)t'$. New reduction: 
%% $(\underline{\lambda}x.t)t' \lstep{\beta} [t'/x]t$

%% $(\lambda x.t)t' \lstep{\beta} [t'/x]t$
%% \item Contraction $\phi$ and erase function $e$:

%% $(\underline{\lambda}x.t)t' \to_e (\lambda x.e(t))\ e(t')$.

%% $(\underline{\lambda}x.t)t' \to_{\phi} [\phi(t')/x]\phi(t))$.

%% \item

%% \

%%   \begin{tabular}{lllll}

%% \begin{diagram}[size=2em,textflow]
%% t_1' & \rDashtoo_{\underline{\beta}} & t_2' \\
%% \dTo_{e} & &  \dDashto_{e} \\
%% t_1 &  \rOnto_{\beta}  & t_2 \\
%% \end{diagram}

%% &

%% \begin{diagram}[size=2em,textflow]
%% t_1 & \rOnto_{\underline{\beta}} & t_2 \\
%% \dTo_{\phi} & &  \dTo_{\phi} \\
%% \phi(t_1) &  \rDashtoo_{\beta}  & \phi(t_2) \\
%% \end{diagram}
%% &
%% \begin{diagram}[size=1.5em,textflow]
%%  & & t & & \\
%%  & \ldTo^e & & \rdTo^{\phi} &  \\
%% e(t) & & \rDashtoo_{\beta} &  & \phi(t) \\
%% \end{diagram}
%%  \\   
%%   \end{tabular}

%% \end{itemize}  
%% \end{frame}

%% \begin{frame}
%% \frametitle{Confluence: Barendregt's labelling method}

%% \
%%   \begin{tabular}{lllll}

%% \begin{diagram}[size=2em,textflow]
%% t_1' & \rDashtoo_{\underline{\beta}} & t_2' \\
%% \dTo_{e} & &  \dDashto_{e} \\
%% t_1 &  \rOnto_{\beta}  & t_2 \\
%% \end{diagram}

%% &

%% \begin{diagram}[size=2em,textflow]
%% t_1 & \rOnto_{\underline{\beta}} & t_2 \\
%% \dTo_{\phi} & &  \dTo_{\phi} \\
%% \phi(t_1) &  \rDashtoo_{\beta}  & \phi(t_2) \\
%% \end{diagram}
%% &
%% \begin{diagram}[size=1.5em,textflow]
%%  & & t & & \\
%%  & \ldTo^e & & \rdTo^{\phi} &  \\
%% e(t) & & \rDashtoo_{\beta} &  & \phi(t) \\
%% \end{diagram}
%%  \\   
%%   \end{tabular}

%% Proof of strip property:
%% \begin{diagram}[size=3em,textflow]
%%  & & t & & & \\
%%  & \ldTo^{\beta} & \uTo^e & \rdOnto^{\beta} &  & \\
%% t_1 &  \lTo_{\phi} &   t_3 & &  t_2\\
%%  & \rdDashtoo_{\beta}  & & \rdDashtoo_{\underline{\beta}} \ldDashtoo^{\beta} &  \uDashto_e \\
%%  & & t'  & \lTo_{\phi} & t_4 \\
%% \end{diagram}

%% \end{frame}

\begin{frame}
\frametitle{Confluence: Hardin's Interpretation method}
\begin{itemize}
\item Assumption I: $\to \ := \to_1 \cup \to_2$ and $\to_1$ is strongly normalizing and confluent.
\item Assumption II:$\to_i \subseteq \to$ is defined on $\to_1$ normal form $\nu(t)$.
\item Assumption III: If $a \to_2 b$, then $\nu(a) \to_i \nu(b)$. 
\item Then: Confluence of $\to_i$ implies confluence of $\to$.

\item

\begin{diagram}[size=1.5em,textflow]
& & & & a & & & &\\
& & &\ldLine &  & \rdLine & & &\\
& &\ldLine & &  & & \rdLine & &\\
&\ldOnto & & & \dDashtoo^1 &  &  & \rdOnto & \\
a'& &  & & \nu(a)  &  & & & a'' \\
&\rdDashtoo^1 &  &\ldDashtoo^i &   & \rdDashtoo^i  &  & \ldDashtoo^1 &\\
& & \nu(a')  &  &   &  & \nu(a'') & & \\
& &  & \rdDashtoo^i  &  & \ldDashtoo^i &   &  & \\
& &  &  & b  &   &  & & \\
\end{diagram}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Hardin's Interpretation method: Applications}

\begin{itemize}
%% \item Confluence of $(\Lambda, \to_{\beta}, \to_{\eta})$ with:

%% $\lambda x.t\ x \to_{\eta} t$, where $x$ is not free in $t$. 
%% \item Traditionally can also showed by Hindley-Rosen's method.
\item Confluence of $(\Lambda_{\mu}, \to_{\beta}, \to_{\mu})$, originated from $\mathsf{Selfstar}$.

\item $\Lambda_{\mu}$ denotes terms $t \ :: = \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ \mu t$.

\item Closure: $\mu \ ::= \M{x}{t}{\mathcal{I}}$. Locality.

\item New reductions: 

\

  \begin{tabular}{ll}
 \infer{\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}
&
 \infer{\mu t \to_{\mu} t}{dom(\mu) \# \mathsf{FV}(t)}

\\
\\

 \infer{ \mu(\lambda x.t) \to_{\mu} \lambda x.\mu t}{}

&

\infer{ \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu t_2)}{}
\\    
  \end{tabular}


\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Typed Lambda Calculus and Lambda Encoding
%\item Typed Lambda encoding
\item Type Preservation and Confluence
\item \remph{Limits of Dependent type}
\item Selfstar
\item Summary
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Limits of Dependent Type}

How to show some formula is unprovable.
\begin{itemize}
\item Formalized the notion of proof. 


\item If there is a proof of $\bot$, then draw a contradiction at meta-level.


\item Under Curry Howard correspondent, showing some type is uninhabited.


\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Limits of Dependent Type}

Recall second order dependent type: 
\begin{itemize}
\item<1-> Type as expression: 
$T \ := X\ | \ \forall X:\kappa.T\ | \ T_1 \to T_2\ | \ \Pi x:T_1.T_2\ | \ T\ t$

Kind as expression $\kappa \ := * \ | \ \xi x:T.\kappa$

\item<2-> Induction principle:

\footnotesize{$\forall P: (\xi x: \mathsf{Nat}.*). P\ 0 \to (\Pi y:\mathsf{Nat}. (P \ y) \to (P\ (\mathsf{S}\ y))) \to \Pi x:\mathsf{Nat}.P\ x$}

\item<3-> 
\small{$P:(\xi x: \mathsf{Nat}.*), a : P\ 0, b : \Pi y:\mathsf{Nat}. (P \ y) \to (P\ (\mathsf{S}\ y)), x:\mathsf{Nat} \vdash (b\ 1\ (b\ 0\ a)): P\ (\mathsf{S}\ 1)$}

Induction is not derivable(provable) within Dependent type system\footnote{Coquand's Metamathematical investigations of a calculus of constructions}

\item<4-> Since $\bot$ is uninhabit, can not inhabit types like $T \to \bot$, where $T$ is inhabited. Thus can not prove $0 \not = 1$.\footnote{Werner's A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}
\item<5-> These compromise the usage of Church encoding in dependent type system.
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Typed Lambda Calculus and Lambda Encoding
%\item Typed Lambda encoding
\item Type Preservation and Confluence
\item Limits of Dependent type
\item \remph{Selfstar}
\item Summary
\end{itemize}

\end{frame}


\begin{frame}
\frametitle{$\mathsf{Selfstar}$: I}
\begin{itemize}

\item Recall that:
\footnotesize{$x:\mathsf{Nat} \vdash \cemph{\bar{n}} : \forall P: (\xi x: \mathsf{Nat}.*). P\ 0 \to (\Pi y:\mathsf{Nat}. (P \ y) \to (P\ (\mathsf{S}\ y))) \to P\ \cemph{\bar{n}}$, for any Church numerals $\bar{n}$ }

\item Dependent type system, namely, $\Pi$ construct can not grasp this level of quantification.

\item One way to try to capture(with the help of recursion) this is:

\footnotesize{$x:\mathsf{Nat} \vdash \cemph{\bar{n}} : \cemph{\iota x}.\forall P: (\xi x: \mathsf{Nat}.*). P\ 0 \to (\Pi y:\mathsf{Nat}. (P \ y) \to (P\ (\mathsf{S}\ y))) \to P\ \cemph{x}$}

\footnotesize{$\mathsf{Nat}\ := \cemph{\iota x}.\forall P: (\xi x: \mathsf{Nat}.*). P\ 0 \to (\Pi y:\mathsf{Nat}. (P \ y) \to (P\ (\mathsf{S}\ y))) \to P\ \cemph{x}$}
\item add two typing rules: 

  \begin{tabular}{ll}
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}


&
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T}
\\    
  \end{tabular}
\item Introduce closure $\mu\ := \ \M{x}{t}{\mathcal{I}} \cup \M{X}{T}{\mathcal{N}}$
\item Wrap around term and type, $\mu t, \mu T$, $\tilde{\mu} \in \Gamma$. 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{$\mathsf{Selfstar}$: II}
Church encoding and Scott encoding in $\mathsf{Selfstar}$
\begin{itemize}

\item Church encoding($\tilde{\mu_c}$):

\noindent $(\remph{\mathsf{Nat}:*} ) \mapsto$

\footnotesize{$ \iota x. \Pi C: \mathsf{Nat} \to *.  (\Pi n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to (C\ 0) \to (C\ x)$}

\noindent $(\remph{\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat}} )\mapsto \lambda n.\lambda C. \lambda s.\lambda z. s \ \remph{n}\ (n\ C\ s\ z)$

\noindent $(\remph{0:\mathsf{Nat}})  \mapsto \lambda C. \lambda s. \lambda z.z$.

\item Scott encoding($\tilde{\mu_s}$):

\noindent $(\remph{\mathsf{Nat}:*} ) \mapsto \iota x. \Pi C: \mathsf{Nat} \to *.  (\Pi n : \mathsf{Nat}.C\ (\mathsf{S}\ n)) \to (C\ 0) \to (C\ x)$

\noindent $(\remph{\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat}} )\mapsto \lambda n.\lambda C. \lambda s.\lambda z. s \ n$

\noindent $(\remph{0:\mathsf{Nat}})  \mapsto \lambda C. \lambda s. \lambda z.z$


\end{itemize}  
\end{frame}

\begin{frame}
\frametitle{$\mathsf{Selfstar}$: II}

\begin{itemize}
\item Induction principle for Church encoding:

$ \tilde{\mu_c} \vdash (\remph{\mathsf{Ind}}\ :=\lambda C. \lambda s.\lambda z. \lambda n. n\ C\ s\ z): $

\noindent \footnotesize{$\Pi C: \mathsf{Nat} \to *. \Pi n:\mathsf{Nat}.((C\ n)\to (C\ (\mathsf{S}\ n))) \to C\ 0 \to \Pi n:\mathsf{Nat}. C\ n$}  
 
\item Addition function:

\noindent $\tilde{\mu_c} \vdash (\remph{\mathsf{add}}:= \lambda n. \lambda m. \mathsf{Ind}\ (\lambda y.\mathsf{Nat})\ (\lambda x.\mathsf{S})\ m\ n) : \mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Nat}$.

\item Case analysis principle for Scott encoding:

\noindent $\tilde{\mu_s} \vdash (\remph{\mathsf{Case}}\ := \lambda C. \lambda s.\lambda z. \lambda n. n\ C\ s\ z):$

\noindent $ \Pi C: \mathsf{Nat} \to *. \Pi n:\mathsf{Nat}. (C\ (\mathsf{S}\ n)) \to C\ 0 \to \Pi n:\mathsf{Nat}. C\ n$

\item addition function:

$(\remph{\mathsf{add}: \mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Nat}} ) \mapsto \lambda n.\lambda m. \mathsf{Case}\ (\lambda n.\mathsf{Nat})\ \ (\lambda p . (\mathsf{S}\ (\mathsf{add}\ p\ m)) )\ m\ n $ 

\end{itemize}  
\end{frame}

\begin{frame}
\frametitle{$\mathsf{Selfstar}$: III}

\begin{itemize}
\item Due to $*:*$ and recursive defintion, term does not correspond to proof, type does not correspond to formula. 
\item Future work: show a fragment of $\mathsf{Selfstar}$ that can be erased to $\mathsf{F}^{\omega}$.
%\item<4-> Future work (II): identify a semantics for type. 
\end{itemize}  
\end{frame}
\begin{frame}
\frametitle{Outline}

\begin{itemize}
\item Typed Lambda Calculus and Lambda Encoding
%\item Typed Lambda encoding
\item Type Preservation and Confluence
\item Limits of Dependent type
\item Selfstar
\item \remph{Summary}
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Summary}

\begin{itemize}
\item We seen Church and Scott encoding data and as alternatives to 
implement algebraic data type.
\item The use of confluence in preservation proof.
\item Several methods to prove confluence.
\item Limits of dependent type system give rise to $\mathsf{Selfstar}$. 
\item Introduced $\mathsf{Selfstar}$. 

\end{itemize}  
\end{frame}

\begin{frame}
\frametitle{Last But Not Least}

\begin{itemize}
\item Thank my advisor Prof. Aaron Stump.

\item Thank my exam committee: 

Prof. Cesare Tinelli, Prof. Kasturi Varadarajan, Prof. Ted Herman, Prof. Douglas Jones.

\item For all the audiences.

\end{itemize}  
\end{frame}


\end{document}



